SHOW AXIOM WISEMAN;
ASSUME A(WISE3,RW,W1);
CANCEL;
SHOW STEP FOOL2;
SHOW PROOF FOOL2;
SHOW PROOF KW1;
SHOW PROOF;
SHOW AXIOM WISEMAN;
ASSUME A(WISE3,RW,W1);
CANCEL;
∀E KNOWTRUE FOOL KW(WISE3,WHITE1) RW;
∀E KNOWTRUE FOOL KW(WISE3,WHITE2) RW;
∀E KW1 WISE3 WHITE1 RW;
∀E KW1 WISE3 WHITE2 RW;
TAUT 33:#2 WISEMAN1 WISEMAN6 31 33;
TAUT 34:#2 WISEMAN1 WISEMAN7 32 34;
ASSUME A(WISE3,RW,W1);
∀E KNOW WISE3 WHITE1 RW;
∀E KNOW WISE3 WHITE2 RW;
TAUT 38:#2 35 38;
TAUT 39:#2 36 39;
∀E 40 W1;
∀E 41 W;
CANCEL;
∀E 41 W1;
MP 37 42;
MP 37 43;
SHOW AXIOM WISEMAN;
∀E FOOLTRANS WISE3 KW(WISE1,WHITE2) RW W1;
∀E FOOLTRANS WISE3 KW(WISE1,WHITE3) RW W1;
∀E FOOLTRANS WISE3 KW(WISE2,WHITE1) RW W1;
∀E FOOLTRANS WISE3 KW(WISE2,WHITE3) RW W1;
∀E FOOLTRANS WISE3 KW(WISE2,KW(WISE1,WHITE1)) RW W1;
TAUT 46:#2 WISEMAN2 46 37;
TAUT 47:#2 WISEMAN3 47 37;
TAUT 48:#2 WISEMAN4 48 37;
TAUT 49:#2 WISEMAN5 49 37;
TAUT 50:#2 WISEMAN10 50 37;
SHOW AXIOM WISEMAN;
EXIT;CANCEL 37;
SHOW PROOF;
∀E KW WISE3 KW(WISE2,WHITE2) RW;
∀E KNOWTRUE WISE3 KW(WISE2,WHITE2) RW;
TAUT 37:#2#2 37 38 WISE12;
TAUT 37:#2#2 37 38 WISEMAN12;
∀E KNOWTRUE FOOL KW(WISE3,KW(WISE2,WHITE2)) RW;
TAUT 37:#2#2 37 38 39 WISEMAN9 WISEMAN12;
CANCEL;
SHOW AXIOM NOT;
SHOW AXIOM FOOL;
EXIT;fetch know.ax;